%:- op(1150,  fx, (package)). 

:- package 'edu.cmu.cs.erl.rules'.


%%%Some utilities for us to use.
%Booleans
boolean(true, Obj) :- java_get_field('java.lang.Boolean', 'TRUE', Obj).
boolean(false, Obj) :- java_get_field('java.lang.Boolean', 'FALSE', Obj).

%Strings
string([], Obj) :- java_constructor('java.lang.String'(), Obj).
string([T1|Ts], Str) :-
   string(T1, FirstStr),
   string(Ts, BaseStr),
   java_method(FirstStr, concat(BaseStr), Str).
string(Str, Obj) :- java_constructor('java.lang.String'(Str), Obj).

integer(Proint,Javint):-java_get_field('java.lang.Integer','',Javint).

addErrorEnding([], Suffix, []).
addErrorEnding([(X, Message)|Errors], Suffix, [(X, NewMessage)|CompletedErrors]) :-
   java_method(Message, concat(Suffix), NewMessage),
   addErrorEnding(Errors, Suffix, CompletedErrors).

setResponsibleObject([], Object, []).
setResponsibleObject([(null, Message)|Errors], Object, [(Object, Message)|SetErrors]) :-
	setResponsibleObject(Errors, Object, SetErrors).
setResponsibleObject([(X, Message)|Errors], Object, [(X, Message)|SetErrors]) :-
	X \== null,
	setResponsibleObject(Errors, Object, SetErrors).
	
combineErrors([(_, Message)], Message).
combineErrors([(_, Message) | Errors], CompleteMessage) :-
   combineErrors(Errors, OtherMessages),
   java_method(OtherMessages, concat(', and '), Temp),
   java_method(Temp, concat(Message), CompleteMessage).

%%% Main checks
	  
%And
check(G, M,and(P1,P2),E):-
	check(G, M,P1,E1),
	check(G, M,P2,E2),
	append(E1,E2,E).
	
%Imp-t2
check(G, M,implies(P1,P2),[]):-
	check(G, M,P1,[E1|E1s]).

%Imp-t1
check(G, M,implies(P1,P2),[]):-
	check(G, M,P1,[]),
	check(G, M,P2,[]).

%Imp-f
check(G, M,implies(P1,P2),Errors):-
	check(G, M,P1,[]),
	check(G, M,P2,[SubE|SubErrors]),
	getIsMessage(G, M, P1, Str),
	addErrorEnding([SubE|SubErrors], ' since ', Temp),	
	addErrorEnding(Temp, Str, Errors).
% P2 should be equal to *correct thing* since P1 is equal to *correct thing*
	
%Or-t1
check(G, M,or(P1,P2),[]):-
	check(G, M,P1,E),
	check(G, M,P2,[]).

%Or-t2
check(G, M,or(P1,P2),[]):-
	check(G, M,P1,[]),
	check(G, M,P2,E).

%Or-f
check(G, M,or(P1,P2),[(null, Message)]):-
	check(G, M,P1,[E1|E1s]),
	check(G, M,P2,[E2|E2s]),
	combineErrors([E1|E1s], Message1),
	combineErrors([E2|E2s], Message2),
	java_method(Message1, concat(' or '), Temp),
	java_method(Temp, concat(Message2), Message).
	  
%Atomic	  
check(G,M,at(X), E) :-
	java_method('edu.cmu.cs.erl.ERL', evaluate(M,G,X), BObj),
	boolean(B, BObj),
	B = true ->
	  E=[] ;
	  java_method('edu.cmu.cs.erl.ERL', getMessage(M,G,X), Str),
	  E=[(null,Str)].	

%Forall-lazy
check(G, M, forallLazy(X, Name, LazyList, P), E) :-
   java_method('edu.cmu.cs.erl.ERL', getList(M, G, LazyList), List),
   check(G, M, forall(X, Name, LazyList, List, P), E).

%Forall-2
check(G,M,forall(X,Name,List,[],P),[]).

%Forall-1
check(G,M,forall(X,Name,List, [A|As],P),E):-
	copy_term(forall(X,Name, As,P),R),
	X=A,
	put_term(G, Name, A),
	check(G,M,P,E1),
	check(G,M,R,F),
	setResponsibleObject(E1, A, E2),
	append(F,E2,E).

%Exists-lazy
check(G, M, existsLazy(X, Name, LazyList, P), E) :-
   java_method('edu.cmu.cs.erl.ERL', getList(M, G, LazyList), List),
   check(G, M, exists(X, Name, LazyList, List, P), E).

%Exists
check(G,M,exists(X,Name, List, [],P),[(null,Message)]):-
    getIsMessage(G, M, P, Str),
    write('in exists check'), nl,
    getMessage(G, M, at(List), ListStr),
    string('there must exist a ', T1),
    java_method(T1, concat(Name), T2),
    java_method(T2, concat(' in '), T3),
    java_method(T3, concat(ListStr), T4),
    java_method(T4, concat(' such that '), T5),
    write('in exists at end of message writing'), nl,flush_output,
    java_method(T5, concat(Str), Message).

check(G,M,exists(X, Name, List, [A|As],P),[]):-
	X=A,
	put_term(G, Name, A),
	check(G,M,P,[]),
	put_term(G, Name, []).		
    
check(G,M,exists(X, Name, List, [A|As],P),F):-
	copy_term(exists(X,Name, List, As,P),R),
	X=A,
	put_term(G, Name, A),
	check(G,M,P,E1),
	put_term(G, Name, []),
	check(G,M,R,F).
			

%Not-and
check(G,M,not(and(P1,P2)),E):-
	check(G,M,or(not(P1),not(P2)),E).

%Not-or
check(G,M,not(or(P1,P2)),E):-
	check(G,M,and(not(P1),not(P2)),E).
	
%Not-not
check(G,M,not(not(P)),S):-
	check(G,M,P,S).
	
%Not-Forall
check(G,M,not(forall(X,Name,As,P)),E):-
check(G,M,exists(X,Name,_,As,not(P)),E).

%Not-Exists
check(G,M,not(exists(X,Name, _,As,P)),E):-
check(G,M,forall(X,Name,As,not(P)),E).

%Not-Atomic
check(G,M,not(at(X)),E):-
	java_method('edu.cmu.cs.erl.ERL', evaluate(M, G, X), BObj),
	boolean(B, BObj),
	B = false ->
	  E=[] ;
	  java_method('edu.cmu.cs.erl.ERL', getNotMessage(M, G, X), Str),
	  E=[(null,Str)].	

getMessage(G, M, at(P), Message) :-
    java_wrap_term(P, PJava),
   java_method('edu.cmu.cs.erl.ERL', getMessage(M, G, PJava), Message).

getMessage(G, M, and(P1, P2), Message) :-
   getMessage(G, M, P1, M1),
   getMessage(G, M, P2, M2),
   java_method(M1, concat(' and '), T1),
   java_method(T1, concat(M2), Message).

%getNotMessage(G, M, at(P), Message) :-
%   java_wrap_term(P, PJava),
%   java_method('edu.cmu.cs.erl.ERL', getNotMessage(M, G, PJava), Message).

%getNotMessage(G, M, and(P1, P2), Message) :-
%   getNotMessage(G, M, P1, M1),
%   getNotMessage(G, M, P2, M2),
%   java_method(M1, concat(' and '), T1),
%   java_method(T1, concat(M2), Message).


getIsMessage(G, M, at(P), Message) :-
   java_wrap_term(P, PJava),
   java_method('edu.cmu.cs.erl.ERL', getIsMessage(M, G, PJava), Message).

getIsMessage(G, M, and(P1, P2), Message) :-
   getIsMessage(G, M, P1, M1),
   getIsMessage(G, M, P2, M2),
   java_method(M1, concat(' and '), T1),
   java_method(T1, concat(M2), Message).

getIsMessage(G, M, or(P1, P2), Message) :-
   getIsMessage(G, M, P1, M1),
   getIsMessage(G, M, P2, M2),
   java_method(M1, concat(' or '), T1),
   java_method(T1, concat(M2), Message).
   
getIsMessage(G,M, implies(P1,P2), Message):-
   getIsMessage(G,M,P1,M1),
   getIsMessage(G,M,P2,M2),
   java_method(M1, concat(' implies that '), T1),
   java_method(T1, concat(M2), Message).
   
getIsMessage(G,M,exists(X,Name, List, _,P),Message):-
    getIsMessage(G, M, P, Str),
    write('between getis and get'),nl,
    getMessage(G, M, at(List), ListStr),
    string('there exists ', T1),
    java_method(T1, concat(Name), T2),
    java_method(T2, concat(' in '), T3),
    java_method(T3, concat(ListStr), T4),
    java_method(T4, concat(' such that '), T5),
    write('at end of getis'),nl,flush_output,
    java_method(T5, concat(Str), Message).
    
getIsMessage(G,M,existsLazy(X,Name, List, _,P),Message):-
    getIsMessage(G,M,exists(X,Name, List, _,P),Message).

getIsMessage(G,M,forall(X,Name, List, _,P),Message):-
	getIsMessage(G, M, P, Str),
    getMessage(G, M, at(List), ListStr),
    string('forall ', T1),
    java_method(T1, concat(Name), T2),
    java_method(T2, concat(' in '), T3),
    java_method(T3, concat(ListStr), T4),
    java_method(T4, concat(' , '), T5),
    java_method(T5, concat(Str), Message).

getIsMessage(G,M,forallLazy(X,Name, List, _,P),Message):-
	getIsMessage(G,M,forall(X,Name, List, _,P),Message).
   
getIsMessage(G, M, not(P), Message) :-
   getIsNotMessage(G, M, not(P), Message).
   
getIsNotMessage(G, M, not(P), Message) :-
   java_wrap_term(P, PJava),
   java_method('edu.cmu.cs.erl.ERL', getIsNotMessage(M, G, PJava), Message).


%%%Prolog tests
returnTest(X, X).

boolTest(X, S) :- boolean(true, X), string('True String', S).
boolTest(X, S) :- boolean(false, X), string('False String', S).

intTest(X, 0) :- X < 5.
intTest(X, 1) :- X >= 5.

intToStringTest(Int, String):-
   Int < 5, string('X is less than 5', String).
intToStringTest(Int, String):-
   Int >= 5, string('X is >= than 5', String).

stringTest(String) :- string(['hello',' world!'], String).
	
stringToIntTest(X,Y):-
	java_method('java.lang.Integer',parseInt(X),Y).

stringToBoolTest(X,Y):-
	java_method('edu.cmu.cs.erl.pltests.StringToBoolean',strToBool(X),BOOL),
	boolean(Z,BOOL),
	Z = true -> string('UPPER',Y);
				string('lower',Y).
				
stringsToStringTest(Y):-
	java_method('edu.cmu.cs.erl.pltests.StringsToString',str1(),X1),
	java_method('edu.cmu.cs.erl.pltests.StringsToString',str2(),X2),
	java_method('edu.cmu.cs.erl.pltests.StringsToString',str3(),X3),
	X=[X1|[X2|[X3]]],
	string(X,Y).
